DDD[1,3] - www.SailDart.org

perm filename DDD[1,3] blob sn#248485 filedate 1976-11-20 generic text, type T, neo UTF8
(DEFPROP DEF (((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))~
 (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PL~
US Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (~
!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (~
DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B))~
 (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE ~
DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE~
 DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!M~
ULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)~
) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9)~
 ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS ~
C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (~
!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS ~
A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_~
INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_~
PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF~
 (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2~
) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) IN~
FERENCE_RULES) 
(DEFPROP DEFNIL (((DEF NIL) NIL PROVABLE DEFNIL) ((DEF NIL) NIL PROVABLE DEFNIL)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A)~
 (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF ~
(!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POI~
NTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))~
) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!~
PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS ~
B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) ~
(DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ~
((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS ~
A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (~
!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!~
PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PR~
OVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF~
7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!~
CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS ~
A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (~
!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100~
) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF N~
IL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF0 (((DEF 0) NIL PROVABLE DEF0) ((DEF 0) NIL PROVABLE DEF0)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!AN~
Y (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS~
 E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF~
 (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVID~
E (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16)~
 ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF~
 (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A)~
)) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!P~
V_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!~
MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)~
) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS ~
A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLU~
S B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF~
 (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PL~
US A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1~
)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!A~
RRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 10~
0)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0~
) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF1 (((DEF 1) NIL PROVABLE DEF1) ((DEF 1) NIL PROVABLE DEF1)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL~
 PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF ~
(!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTE~
R (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) P~
ROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV~
_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF~
15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -~
1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) ~
(DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A~
))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVAB~
LE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!~
PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF~
 (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (~
!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS ~
I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVA~
BLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((D~
EF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_P~
LUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1~
) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF2 (((DEF 2) NIL PROVABLE DEF2) ((DEF 2) NIL PROVABLE DEF2)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL~
 PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I~
)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_~
PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ~
 (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A))~
 (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B~
)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABL~
E DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVAB~
LE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (~
!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS ~
A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF~
9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLU~
S C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS~
 (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLU~
S A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRA~
Y_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!P~
V_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (D~
EF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF~
 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) ~
INFERENCE_RULES) 
(DEFPROP DEF3 (((DEF 100) NIL PROVABLE DEF3) ((DEF 100) NIL PROVABLE DEF3)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS ~
I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVA~
BLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!~
DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))~
) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!C~
ONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!~
PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((D~
EF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!P~
LUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (~
!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PL~
US A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT~
 (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (D~
EF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A)))~
 PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)~
) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!P~
V_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A~
) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (~
!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY~
_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) ~
PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NI~
L PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF4 (((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS~
 I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_~
PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF~
4)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5)~
 ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!~
PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((D~
EF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (~
!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DE~
F20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PL~
US Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!~
PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS ~
B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1~
 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!P~
V_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVA~
BLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B)~
 (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!P~
V_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF~
8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_P~
LUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) P~
ROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A~
1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF~
 (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_P~
LUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4~
) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DE~
F0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF5 (((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5~
) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5)) I_RULES_NA~
MED) 
(DEFPROP DEF (((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A~
1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF~
 (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_P~
LUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4~
) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DE~
F0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS~
 E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV~
_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y~
) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_P~
LUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS~
 A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((D~
EF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((~
DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_P~
LUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!P~
V_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!P~
V_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PL~
US A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B~
) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRA~
Y_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV~
_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) ~
PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS~
 I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROV~
ABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RU~
LES) 
(DEFPROP DEF6 (((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS ~
A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!CONCAT (!PV_PLUS A1) (!ARR~
AY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!P~
V_PLUS I))))) PROVABLE DEF6)) I_RULES_NAMED) 
(DEFPROP !LE (((!LE 1 (!PV_PLUS I)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE1) ((!LE~
 (!PV_PLUS I) 100) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE2) ((!LE 1 (!PV_PLUS I)) ~
(DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE1)) INFERENCE_RULES) 
(DEFPROP LE1 (((!LE 1 (!PV_PLUS I)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE1) ((!LE~
 1 (!PV_PLUS I)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE1)) I_RULES_NAMED) 
(DEFPROP !LE (((!LE (!PV_PLUS I) 100) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE2) ((!~
LE 1 (!PV_PLUS I)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE1) ((!LE (!PV_PLUS I) 100~
) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE2) ((!LE 1 (!PV_PLUS I)) (DEF (!CONCAT (!P~
V_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE1)) INFERENCE_RULES) 
(DEFPROP LE2 (((!LE (!PV_PLUS I) 100) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE2) ((!~
LE (!PV_PLUS I) 100) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) PROVABLE LE2)) I_RULES_NAMED) 
(DEFPROP TR (((TR 0) NIL PROVABLE NIL) ((TR 0) NIL PROVABLE NIL)) INFERENCE_RULES) 
(DEFPROP NIL (((TR 0) NIL PROVABLE NIL)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF~
7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!~
CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS ~
A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (~
!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100~
) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF N~
IL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AN~
D (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (~
!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS~
 N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!N~
EQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVA~
BLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (~
!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PL~
US B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV~
_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)))~
 PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) ~
(DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!A~
ND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS~
 A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!P~
V_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))~
) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DE~
F5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1~
 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ~
((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF7 (((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DE~
F7) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7)) I_RULE~
S_NAMED) 
(DEFPROP DEF (((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) ~
(DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_~
PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) ~
(!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!A~
ND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_I~
NDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PR~
OVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL ~
PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)~
) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_P~
LUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ ~
(!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) ~
(DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)~
) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE~
 DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABL~
E DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!~
MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A~
)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9~
) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS~
 C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS ~
(!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS~
 A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY~
_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV~
_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DE~
F (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF ~
2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) I~
NFERENCE_RULES) 
(DEFPROP DEF7A (((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)~
) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS~
 A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS ~
B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) (~
(DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONC~
AT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLU~
S A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1~
)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_~
PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE ~
DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABL~
E DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLU~
S A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_P~
LUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE ~
DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B)~
 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DE~
F (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_P~
LUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!M~
ULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROV~
ABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10~
) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!P~
V_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PL~
US A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DE~
F (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!~
AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6~
) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CON~
CAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) ~
(!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PR~
OVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF8 (((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PV_PLUS A)) (D~
EF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DE~
F (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND ~
(DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A)~
)) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_P~
LUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) P~
ROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5)~
 ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!~
PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((D~
EF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (~
!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DE~
F20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PL~
US Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!~
PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS ~
B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1~
 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!P~
V_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVA~
BLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B)~
 (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!P~
V_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF~
8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_P~
LUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) P~
ROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A~
1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF~
 (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_P~
LUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4~
) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DE~
F0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF9 (((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS B)) (D~
EF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF~
10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (~
!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_~
PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (~
DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) ~
(!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DE~
F6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!C~
ONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)~
) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL ~
PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A~
) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF~
 (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!PO~
INTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B)~
)) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (~
!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS~
 B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A))~
 (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12)~
 ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS~
 A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) ~
(!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (~
!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) P~
ROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DE~
F7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (~
!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS~
 A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) ~
(!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 10~
0) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF ~
NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF10 (((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE D~
EF10) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10)) I_R~
ULES_NAMED) 
(DEFPROP DEF (((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS~
 B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS ~
(!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE ~
DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!P~
V_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))~
) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLU~
S A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MORE~
DEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!P~
V_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE D~
EF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE~
 DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_P~
LUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (~
!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLU~
S Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!P~
V_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_P~
LUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ~
((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13)~
 ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!P~
V_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF ~
(!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF ~
(!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV~
_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLU~
S B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!A~
RRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (~
!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A)~
)) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_P~
LUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL P~
ROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE~
_RULES) 
(DEFPROP DEF11 (((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!PV_PLUS A)) ~
(DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (D~
EF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_P~
LUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE~
 DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV~
_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!~
PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV~
_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!~
ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF~
 (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)~
) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) (~
(DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNI~
L) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (~
DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y))~
)) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ~
((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PR~
OVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_~
PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B))~
 (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!P~
V_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DE~
F11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF~
 (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS ~
B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) ~
(DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_~
PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MO~
REDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF~
 (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!P~
V_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!~
PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE ~
DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF12 (((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS B)) ~
(DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) P~
ROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (~
DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_~
PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABL~
E DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!P~
V_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (~
!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!P~
V_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (~
!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DE~
F (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A~
)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ~
((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFN~
IL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) ~
(DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)~
))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19)~
 ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) P~
ROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV~
_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)~
) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!~
PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE D~
EF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DE~
F (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS~
 B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A))~
 (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV~
_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (M~
OREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DE~
F (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!~
PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (~
!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE~
 DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF13 (((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)))~
 PROVABLE DEF13) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))~
) PROVABLE DEF13)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLU~
S (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV~
_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (~
!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B~
))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A~
)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) ~
(!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_P~
LUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX ~
(!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)~
)))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE~
 DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!L~
E 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF~
2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TR~
IPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVA~
BLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (~
!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS~
 A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV~
_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!M~
ULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (D~
EF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A)))~
 PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_P~
LUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PL~
US (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVAB~
LE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF ~
(!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS ~
B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_~
PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (M~
OREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX ~
(!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABL~
E DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVA~
BLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF14 (((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!P~
V_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_~
PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B))~
 (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!P~
V_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DE~
F11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF~
 (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS ~
B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) ~
(DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_~
PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MO~
REDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF~
 (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!P~
V_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!~
PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE ~
DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY~
_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT~
 (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!P~
V_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND ~
(DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!M~
ULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV~
_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!P~
V_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!~
PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!A~
ND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS~
 A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!P~
V_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE D~
EF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF~
 (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (~
!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_~
PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DE~
F (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PR~
OVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL ~
PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF15 (((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!P~
V_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_~
PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF1~
5) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1~
 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (~
DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A)~
)) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABL~
E DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!P~
LUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF ~
(!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!~
AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I~
)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVAB~
LE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DE~
F (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PL~
US I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1)~
 NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_P~
LUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ~
((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z)~
 (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PL~
US B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (~
DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV~
_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLU~
S A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE D~
EF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV~
_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLU~
S B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((~
DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C~
))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVAB~
LE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (~
DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV~
_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I~
)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((D~
EF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) (~
(DEF NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF16 (((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!P~
V_PLUS B) 0)) PROVABLE DEF16) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS~
 B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16)) I_RULES_NAMED) 
(DEFPROP !NOT (((!NOT (DEF (!CONCAT (!PV_PLUS Z) (!POINTER NIL)))) NIL PROVABLE DEF17) ((!NOT (DEF (!CONCAT (!EX~
TENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS N))))) NIL PROVABLE DEF18) ((!NOT (DEF (!CONCAT (!PV_PLUS~
 Z) (!POINTER NIL)))) NIL PROVABLE DEF17)) INFERENCE_RULES) 
(DEFPROP DEF17 (((!NOT (DEF (!CONCAT (!PV_PLUS Z) (!POINTER NIL)))) NIL PROVABLE DEF17) ((!NOT (DEF (!CONCAT (!P~
V_PLUS Z) (!POINTER NIL)))) NIL PROVABLE DEF17)) I_RULES_NAMED) 
(DEFPROP !NEQ (((!NEQ (!PV_PLUS P) NIL) (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS P)))) PROVABLE NE1) ((!NE~
Q (!PV_PLUS P) NIL) (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS P)))) PROVABLE NE1)) INFERENCE_RULES) 
(DEFPROP NE1 (((!NEQ (!PV_PLUS P) NIL) (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS P)))) PROVABLE NE1) ((!NEQ~
 (!PV_PLUS P) NIL) (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS P)))) PROVABLE NE1)) I_RULES_NAMED) 
(DEFPROP !NOT (((!NOT (DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS N))))) NIL PROVAB~
LE DEF18) ((!NOT (DEF (!CONCAT (!PV_PLUS Z) (!POINTER NIL)))) NIL PROVABLE DEF17) ((!NOT (DEF (!CONCAT (!EXTENSI~
ON (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS N))))) NIL PROVABLE DEF18) ((!NOT (DEF (!CONCAT (!PV_PLUS Z) (~
!POINTER NIL)))) NIL PROVABLE DEF17)) INFERENCE_RULES) 
(DEFPROP DEF18 (((!NOT (DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS N))))) NIL PROVA~
BLE DEF18) ((!NOT (DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS N))))) NIL PROVABLE D~
EF18)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCA~
T (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_P~
LUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (~
!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS ~
(!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND~
 (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A~
))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!P~
V_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (~
!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PRO~
VABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (D~
EF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PL~
US B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!~
PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND~
 (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_IND~
EX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROV~
ABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PR~
OVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) ~
(!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLU~
S Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!~
PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (D~
EF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) ~
(!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE D~
EF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE ~
DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MU~
LT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A))~
 (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ~
((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C~
) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!~
PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A~
1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_I~
NDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_P~
LUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF ~
(!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2)~
 NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL)) INF~
ERENCE_RULES) 
(DEFPROP DEF19 (((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CON~
CAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!CONCAT (!EX~
TENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLU~
S Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19)) I_RULES_NAMED) 
(DEFPROP DEFRANGE (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE D~
EFR1) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLU~
S E)))) (!AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR6)~
 ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E))~
)) (!AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR5) ((DE~
FRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!~
AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((DEFRANGE 1 (!PLUS (!~
PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1~
 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PL~
US A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANG~
E (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1)) INFERENCE_RULES) 
(DEFPROP DEFR1 (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR~
1) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1)) I_RULES_N~
AMED) 
(DEFPROP DEFRANGE (((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_P~
LUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R~
) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DAT~
A_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANG~
E (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR6) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRI~
PLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!P~
V_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR5) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (~
!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLU~
S R) (!PV_PLUS A))) PROVABLE DEFR4) ((DEFRANGE 1 (!PLUS (!PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_P~
LUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANG~
E 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS~
 (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PL~
US R) (!PV_PLUS L)) PROVABLE DEFR1)) INFERENCE_RULES) 
(DEFPROP DEFR2 (((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS~
 I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)~
) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A~
))) PROVABLE DEFR2)) I_RULES_NAMED) 
(DEFPROP DEFRANGE (((DEFRANGE 1 (!PLUS (!PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_IN~
DEX (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) ~
(!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1)~
 (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L~
)) PROVABLE DEFR1) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS~
 I)) (!PV_PLUS E)))) (!AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PR~
OVABLE DEFR6) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) ~
(!PV_PLUS E)))) (!AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABL~
E DEFR5) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_~
PLUS E)))) (!AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((DEFRANG~
E 1 (!PLUS (!PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))~
) (DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!C~
ONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEF~
R2) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1)) INFERENC~
E_RULES) 
(DEFPROP DEFR3 (((DEFRANGE 1 (!PLUS (!PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX~
 (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PLUS (!PV_PLUS~
 I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1 (!PV_P~
LUS I) (!PV_PLUS A))) PROVABLE DEFR3)) I_RULES_NAMED) 
(DEFPROP DEF (((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV~
_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!~
PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVA~
BLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLU~
S B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ~
((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!~
PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF~
 (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF12) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) ~
PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE D~
EF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS~
 (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!P~
V_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C))) PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND~
 (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))~
) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE ~
DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (~
!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS ~
I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF 100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NI~
L PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DEF NIL) NIL PROVABLE DEFNIL) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS~
 A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((D~
EF (!CONCAT (!EXTENSION (!PV_PLUS Z) (!PV_PLUS N)) (!POINTER (!PV_PLUS Y)))) (!AND (DEF (!CONCAT (!PV_PLUS Z) (!~
POINTER (!PV_PLUS Y)))) (!NEQ (!PV_PLUS Y) (!PV_PLUS N))) PROVABLE DEF19) ((DEF (!DIVIDE (!PV_PLUS A) (!PV_PLUS ~
B))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (!NEQ (!PV_PLUS B) 0)) PROVABLE DEF16) ((DEF (!PV_PLUS B)) (DEF~
 (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) PROVABLE DEF15) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!MULT -1 (!PV_PL~
US B)) (!PV_PLUS A))) PROVABLE DEF14) ((DEF (!PLUS (!MULT -1 (!PV_PLUS B)) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A~
)) (DEF (!PV_PLUS B))) PROVABLE DEF13) ((DEF (!PV_PLUS B)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF1~
2) ((DEF (!PV_PLUS A)) (DEF (!MULT (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF11) ((DEF (!MULT (!PV_PLUS B) (!PV_PL~
US A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE DEF10) ((DEF (!PV_PLUS B)) (DEF (!PLUS (!PV_PLUS B~
) (!PV_PLUS A))) PROVABLE DEF9) ((DEF (!PV_PLUS A)) (DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) PROVABLE DEF8) ((DEF~
 (!PLUS (!PV_PLUS B) (!PV_PLUS C) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B)) (DEF (!PV_PLUS C)))~
 PROVABLE DEF7A) ((DEF (!PLUS (!PV_PLUS B) (!PV_PLUS A))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS B))) PROVABLE ~
DEF7) ((DEF (!CONCAT (!PV_PLUS A1) (!ARRAY_INDEX (!PV_PLUS I)))) (!AND (MOREDEF (!PV_PLUS A) (!PV_PLUS A1)) (DEF~
 (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I))))) PROVABLE DEF6) ((DEF (!PV_PLUS A1)) (!AND (MOREDEF (!PV_PL~
US A) (!PV_PLUS A1)) (DEF (!PV_PLUS A))) PROVABLE DEF5) ((DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))~
) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS I)) (!LE 1 (!PV_PLUS I)) (!LE (!PV_PLUS I) 100)) PROVABLE DEF4) ((DEF ~
100) NIL PROVABLE DEF3) ((DEF 2) NIL PROVABLE DEF2) ((DEF 1) NIL PROVABLE DEF1) ((DEF 0) NIL PROVABLE DEF0) ((DE~
F NIL) NIL PROVABLE DEFNIL)) INFERENCE_RULES) 
(DEFPROP DEF20 (((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!~
PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20) ((DEF (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I~
)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS A)) (DEF (!PV_PLUS E))) PROVABLE DEF20)) I_RULES_NAMED) 
(DEFPROP DEFRANGE (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS~
 I)) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4)~
 ((DEFRANGE 1 (!PLUS (!PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PL~
US I) 1)))) (DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AN~
D (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PR~
OVABLE DEFR2) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1)~
 ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E))~
)) (!AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR6) ((DE~
FRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!~
AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR5) ((DEFRANG~
E (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (~
DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((DEFRANGE 1 (!PLUS (!PV_PL~
US I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1 (!PV~
_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A)~
 (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANGE (!P~
V_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1)) INFERENCE_RULES) 
(DEFPROP DEFR4 (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)~
) (!PV_PLUS E)))) (!AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((~
DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) ~
(!AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4)) I_RULES_NAMED) 
(DEFPROP DEFRANGE (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS~
 I)) (!PV_PLUS E)))) (!AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PR~
OVABLE DEFR5) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) ~
(!PV_PLUS E)))) (!AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((DE~
FRANGE 1 (!PLUS (!PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I)~
 1)))) (DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DE~
F (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABL~
E DEFR2) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1) ((DE~
FRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!~
AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR6) ((DEFRANG~
E (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (~
!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR5) ((DEFRANGE (!P~
V_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (~
!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((DEFRANGE 1 (!PLUS (!PV_PLUS I)~
 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1 (!PV_PLUS~
 I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!AR~
RAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANGE (!PV_PLU~
S L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1)) INFERENCE_RULES) 
(DEFPROP DEFR5 (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)~
) (!PV_PLUS E)))) (!AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVA~
BLE DEFR5) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!P~
V_PLUS E)))) (!AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE D~
EFR5)) I_RULES_NAMED) 
(DEFPROP DEFRANGE (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS~
 I)) (!PV_PLUS E)))) (!AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PR~
OVABLE DEFR6) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) ~
(!PV_PLUS E)))) (!AND (!LT (!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABL~
E DEFR5) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_~
PLUS E)))) (!AND (DEF (!PV_PLUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((DEFRANG~
E 1 (!PLUS (!PV_PLUS I) 1) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))~
) (DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!C~
ONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEF~
R2) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1) ((DEFRANG~
E (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (~
!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR6) ((DEFRANGE (!P~
V_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (!LT (~
!PV_PLUS I) (!PV_PLUS L)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR5) ((DEFRANGE (!PV_PLU~
S L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!PV_PLUS E)))) (!AND (DEF (!PV_P~
LUS E)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE DEFR4) ((DEFRANGE 1 (!PLUS (!PV_PLUS I) 1) (~
!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_INDEX (!PLUS (!PV_PLUS I) 1)))) (DEFRANGE 1 (!PV_PLUS I) (~
!PV_PLUS A))) PROVABLE DEFR3) ((DEFRANGE 1 (!PV_PLUS I) (!PV_PLUS A)) (!AND (DEF (!CONCAT (!PV_PLUS A) (!ARRAY_I~
NDEX (!PV_PLUS I)))) (DEFRANGE 1 (!PLUS (!PV_PLUS I) -1) (!PV_PLUS A))) PROVABLE DEFR2) ((DEFRANGE (!PV_PLUS L) ~
(!PV_PLUS R) (!PV_PLUS A)) (!LT (!PV_PLUS R) (!PV_PLUS L)) PROVABLE DEFR1)) INFERENCE_RULES) 
(DEFPROP DEFR6 (((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)~
) (!PV_PLUS E)))) (!AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVA~
BLE DEFR6) ((DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!ANY (!DATA_TRIPLE (!PV_PLUS A) (!ARRAY_INDEX (!PV_PLUS I)) (!P~
V_PLUS E)))) (!AND (!LT (!PV_PLUS R) (!PV_PLUS I)) (DEFRANGE (!PV_PLUS L) (!PV_PLUS R) (!PV_PLUS A))) PROVABLE D~
EFR6)) I_RULES_NAMED) 
(DEFPROP INRANGE (((INRANGE (!PV_PLUS I) (SUBRANGE (!PV_PLUS T) (!PV_PLUS L) (!PV_PLUS U))) (!AND (!LE (!PV_PLUS~
 L) (!PV_PLUS I)) (!LE (!PV_PLUS I) (!PV_PLUS U))) PROVABLE INR1) ((INRANGE (!PV_PLUS I) (SUBRANGE (!PV_PLUS T) ~
(!PV_PLUS L) (!PV_PLUS U))) (!AND (!LE (!PV_PLUS L) (!PV_PLUS I)) (!LE (!PV_PLUS I) (!PV_PLUS U))) PROVABLE INR1~
)) INFERENCE_RULES) 
(DEFPROP INR1 (((INRANGE (!PV_PLUS I) (SUBRANGE (!PV_PLUS T) (!PV_PLUS L) (!PV_PLUS U))) (!AND (!LE (!PV_PLUS L)~
 (!PV_PLUS I)) (!LE (!PV_PLUS I) (!PV_PLUS U))) PROVABLE INR1) ((INRANGE (!PV_PLUS I) (SUBRANGE (!PV_PLUS T) (!P~
V_PLUS L) (!PV_PLUS U))) (!AND (!LE (!PV_PLUS L) (!PV_PLUS I)) (!LE (!PV_PLUS I) (!PV_PLUS U))) PROVABLE INR1)) ~
I_RULES_NAMED)